OM: Lambda Assembler

Сегодня мы поговорим о том как можно кодировать рекурсивные типы. Как было
показано Вадлером (статья Recursive types for free!) рекурсивные типы легко
решаются, вводится три аксиомы (фиксированая точка fix: (A -> A) -> A, и
аксиомы входа in: F T -> T и выхода из рекурсии out: T -> F T). Мы должны
вводить комбинатор рекурсивной точки как аксиому иначе нам пришлось бы иметь
дело с рекурсивными аксиомами (тут нехватает еще аксиомы функторов для полноты
картины иначе непонятно почему мы можем писать F T). Есть два вида рекурсии:
наименьшей неподвижной точки — рекурсия с терминальным элементов в качестве
базы, и наибольшей неподвижной точки — рекурсия без такое базы, т.е. иначе
говоря бесконечные списки, или коиндуктивные типы, или другими словами
рекурсивные произведения. Индуктивные типы, которые имеют терминальные
элементы, всегда носят эти элементы в качестве компонента суммы, поэтому их
можно назвать рекурсивными суммами, например списки и деревья -- это
рекурсивные суммы.

   data List a = Cons a (List a) | Nil

Хотя работать в пойнт-фри нотации с комбинаторами и решать уравнения можно, в L
так и делается, все же хотелось бы иметь способ избавится от рекурсивных
определений, так как они влияют на редуцироемость термов. Хотелось бы иметь
непрерывную цепочку бета и ета редукций для всех функций. Такое нерекурсивное
кодирование идуктивных типов называется кодированием Боема-Беррардуччи. Оно
напоминает кодирование черча, только примененное для рекурсивных типов.
Рассмотрим типы, как они задаются например в Lean (хотя lean поддерживает
только рекурсивные индуктивные типы, рекурсию в рекордах и коиндукция обычно в
пруверах не поддерживается почему-то).

   type Product (A: *) (B: *) : * = Make (a: A) (b: B)
   type Option  (A: *)        : * = None               | Some (value: A)
   type List    (A: *)        : * = Nil                | Cons (head: A)  (tail: List)
   type Unit                  : * = Make

Тут можно было бы дать полное определение, чтобы были видны синатуры
конструкторов, которые возвращают сам тип как результат выполнения конструктора.

     inductive List (A : Type) : Type :=
             | Nil {} : List A
             | Cons: A → List A → List A

Как показали Боем-Берардуччи такие типы можно кодировать используя
нерекурсивные определения.
Суть состоит в том, чтбы выразить тип как совокупность своих конструкторов,
т.е. чтобы задать функцию над типами, вам нужно задать все функции всех
конструкторов которыми можно сконструировать этот тип. Это механизм
нерекурсивного кодирования индуктивных типов. Вконце вы указываете единичную
функцию которая является foldr комбинатором для этой структуры foldr = id.

( λ (List: * → *)
→ λ (Cons: ∀ (a: *) → a → List a → List a)
→ λ (Nil: ∀ (a: *) → List a)
→ λ (foldr: ∀ (a: *) → List a → ∀ (r: *) → (a → r → r) → r → r)
→ foldr
)

Далее вы выписываете тип, два констркутра и едининую функцию как аргументы
примененные к приведенной выше структуре:

( λ (a : *)
→ ∀ (list : *)
→ (a → list → list) -- Cons
→ list              -- Nil
→ list
)

-- Cons
( λ (a: *)
→ λ (head: a)
→ λ (tail: ∀ (list: *) → (a → list → list) → list → list)
→ λ (list: *)
→ λ (Cons: a -> list → list)
→ λ (Nil: list)
→ Cons head (tail list Cons Nil)
)

-- Nil
( λ (a: *)
→ λ (list: *)
→ λ (Cons: a → list → list)
→ λ (Nil: list)
→ Nil
)

-- foldr
( λ (a: *)
→ λ (tail: ∀ (list: *) -> (a → list → list) → list → list)
→ tail
)

Напишем на Erlang программу которая парсает этот лямбда ассемблер:

    Om/Henk/Morte Core Specification

    EXPR :=                     EXPR             EXPR => {APP,[ I:EXPR, O:EXPR]}
          | "λ"   "(" LABEL ":" EXPR ")" "arrow" EXPR => {LAM,[{ARG:LABEL,I:EXPR, O;EXPR]}
          | "π"   "(" LABEL ":" EXPR ")" "arrow" EXPR => {PI, [{ATH:LABEL,I:EXPR, O;EXPR]}
          |                     EXPR     "arrow" EXPR => {PI, [{"_", I:EXPR, O;EXPR]}
          |           LABEL                           => {VAR,LABEL}
          | "*"                                       => {Star}
          | "[]"                                      => {Box}
          |       "("           EXPR ")"              => EXPR

Само AST языка вот такое (более расширенный язык был описан в статье Henk:
Intermediate Language Эриком Мейером и SPJ в далеком 1997 коду, тут этот язык
больше соотвествует Morte.Turtorial из hackage):

          data Expr a = Const Const
                      | Var   Var
                      | Lam   Text    (Expr a) (Expr a)
                      | Pi    Text    (Expr a) (Expr a)
                      | App  (Expr a) (Expr a)

Вот что получилось:

$ cat priv/List/@

  λ (a: *)
→ ∀ (List: *)
→ ∀ (Cons:
    ∀ (head: a)
  → ∀ (tail: List)
  → List)
→ ∀ (Nil: List)
→ List

{[],
 [{{"λ",a},
   {{const,"*"},
    {{"∀",'List'},
     {{const,"*"},
      {{"∀",'Cons'},

{{{"∀",head},{{var,{a,0}},{{"∀",tail},{{var,{'List',0}},{var,{'List',0}}}}}},
        {{"∀",'Nil'},{{var,{'List',0}},{var,{'List',0}}}}}}}}}}]}

Пока мы умеем только импортировать типы и определения функций, но вроде как бы
больше ничего и не нужно :-) Все типы находятся в своих файлах в файловой
системе. При выполнение бетаредукции программа заново собирается из исходников,
тейпчекается и AST авторедуцируется. Потом это дерево планируется просто
конвертировать в Erlang AST либо LLVM + L runtime.

 > om:a("#List/map") == om:type("List/map").
 true

> om:a("\\(x:*)->\\(y:#List/map)->y").
{lambda,{{arg,x},
         {const,star},
         {lambda,{{arg,y},
                  {lambda,{{arg,a},
                           {const,star},
                           {lambda,{{arg,b},
                                    {const,star},
                                    {lambda,{{arg,f},...

> om:show("priv/List/@").

=INFO REPORT==== 22-Dec-2015::10:01:10 ===
"priv/List/@"
  λ (a: *)
→ ∀ (List: *)
→ ∀ (Cons:
    ∀ (head: a)
  → ∀ (tail: List)
  → List)
→ ∀ (Nil: List)
→ List

{[],
 [{lambda,{{arg,a},
           {const,star},
           {pi,{{arg,'List'},
                {const,star},
                {pi,{{arg,'Cons'},
                     {pi,{{arg,head},
                          {var,{a,0}},
                          {pi,{{arg,tail},
                               {var,{'List',0}},
                               {var,{'List',0}}}}}},
                     {pi,{{arg,'Nil'},
                          {var,{'List',0}},
                          {var,{'List',0}}}}}}}}}}]}

> om:parse(<<"∀ (a: *) → λ (b: * → * → *) → λ (c: * → a) → (((b (c a)) a)
a))"/utf8>>).
{[],
 [{pi,
      {{arg,"a"},
       {const,star},
       {lambda,
           {{arg,"b"},
            {arrow,
                {{const,star},{arrow,{{const,star},{const,star}}}}},
            {lambda,
                {{arg,"c"},
                 {arrow,{{const,star},{var,"a"}}},
                 {app,
                     {{app,
                          {{app,
                               {{var,"b"},
                                {app,{{var,"c"},{var,"a"}}}}},
                           {var,"a"}}},
                      {var,"a"}}}}}}}}}]}

Габриель Гонзалес, автор оригинального Haskell проекта Morte и более
высокоуровневого языка Annah разрабывает свою инфраструктуру с компиляцией в
Haskell. Пока я полностью вдохновился его работой и планирую полностью быть
совместимым с его базовой библиотекой языка Morte, URL типов которого можно
указывать прямо в коде:

$ curl http://sigil.place/talk/1/IO/Monad

λ(a : *) → λ(cmd : #http://sigil.place/talk/1/Cmd #http://sigil.place/talk/1/IO a)
 →  cmd (#http://sigil.place/talk/1/IO  a) (λ(b : *) →
  #http://sigil.place/talk/1/IO/(>>=) b a) (#http://sigil.place/talk/1/IO/pure  a)
__________
[1]. https://github.com/5HT/om
[2]. https://github.com/5HT/om/blob/master/doc/om.pdf